nms1, nms2:(MaName List). Dec(l_disjoint(MaName;nms1;nms2)) 

latex

Definitions	MaName, t  T, type List, x:A. B(x), P  Q, l_disjoint(T;l1;l2), Dec(P)
Lemmas	decidable l disjoint, decidable equal MaName, MaName wf